Using the Algorithm~\ref{alg1} and the theory $\Prov$, we were able to implement
an algorithm that checks if two rules (specified as bipoles) are permutable. 

Given two inference rules
$\rho_1$ and $\rho_2$, we say that $\rho_1$ permutes over $\rho_2$ (denoted
$\rho_1 / \rho_2$) if for all
derivations where $\rho_2$ is applied immediately above $\rho_1$ there is a
derivation where $\rho_1$ is applied immediately above $\rho_2$ (in a bottom up
fashion). The problem of
permutation consists on finding out if two inference rules permute over each
other. 

We will use the theory developed so far to solve this problem. First, using the
Algorithm~\ref{alg1}, we compute the set of derivations $\mathcal{D}_a$ where
$\rho_2$ is applied immediately above $\rho_1$ and the set of derivations
$\mathcal{D}_b$ where $\rho_1$ is applied immediately above $\rho_2$. Note that
if the rule below has multiple premises, there is more than one possible
derivation: one could apply the top rule in any subset of the premises. Secondly, we
use the theory $\Prov$ to verify if: for all derivations $\Xi_i$ in $\mathcal{D}_a$,
there exists a derivation $\Xi_j$ in $\mathcal{D}_b$ such that $\Xi_i
\rightsquigarrow \Xi_j$ (a proof of $\Xi_i$ implies in a proof of $\Xi_j$). If
the result of this verification is positive, we ensure that $\rho_1$ permutes
over $\rho_2$. This algorithm was implemented in OCaml (along with
Algorithm~\ref{alg1}) as part of a bigger project.
It uses \texttt{dlv} \cite{leone06tcl}, an answer-set-programming system, to
find the minimal models of theory
$\Prov$ for two derivations. The proof trees are also generated as \TeX\ files
that can be later compiled to pdf (see Appendix \ref{appendix} for an output
sample). The source code is available at
\url{http://sellf.googlecode.com/files/permutation.tar.gz}. 

% G: Which  ? example?
% Weakening: show that a leaf that has a formula that can be weakened is no
% problem for our setting?
% VN: Here we need to mention the weakening example and how this relates to
% the provIf theory, as well as the $\quest$ example. 


%Our tool basically enumerates all
%possible cases of when $r_2$ can be applied to some open premise $r_2$.
%Then with the help of the propositional solver, it checks, using
%the \tsl{Rules} theories, whether there is a a valid derivation where $r_2$
%is applied last, such that all its premises are still provable, using the
%\tsl{Provif} theories. 

\paragraph{Results}
The implementation was tested with the specifications of linear logic and
intuitionistic logic, in which
the permutation cases are well known and essential for the completeness of
the proof search disciplines focusing and uniform proofs, respectively. 
Our system identified correctly the following cases of permutation for LL:
% neg/neg
$\bindnasrepma / \bindnasrepma$, $\bindnasrepma / \binampersand$, $\binampersand
/ \bindnasrepma$, $\binampersand / \binampersand$,
% pos/pos
$\tensor / \tensor$, $\tensor / \oplus$, $\oplus / \tensor$, $\oplus / \oplus$,
% neg/pos
$\oplus / \bindnasrepma$, $\tensor / \bindnasrepma$, $\oplus / \binampersand$, $\tensor
/ \binampersand$;
% Permutation cases for uniform proofs: guarantee that =>_l can be left to be
% applied in the very end, when the goal is atomic.
and the following cases of permutation for LJ:
$\supset_l / \supset_r$, $\supset_l / \wedge_r$,
$\supset_l / \wedge_l$.

In order to test the ability of identifying permutations when one of the
derivations have formulas that can be weakened, consider as an example the
following inference rules and proof transformations:
{\small
\[
\infer[\circ]{\Gamma, \circ A \vdash \Delta}{\Gamma \vdash A, \Delta}
\;\;\;\;
\infer[\square]{\Gamma \vdash \Delta, \square A}{\Gamma \vdash A}
\]
}%
The two trees generated by applying $\circ$ over $\square$ and vice-versa are:
\begin{small}
\[
\infer[\square]{\Gamma, \circ A \vdash \Delta, \square B}
{
  \infer[\circ]{\Gamma, \circ A \vdash B}{\Gamma \vdash A, B}
}
\;\;\;\;
\infer[\circ]{\Gamma, \circ A \vdash \Delta, \square B}
{
  \infer[\square]{\Gamma \vdash \Delta, A, \square B}{\Gamma \vdash B}
}
\]
\end{small}%
If we consider a calculus in which formulas on both sides of the sequent can
suffer contraction and weakening, these two rules should be permutable. Our
system was able to identify this permutation correctly.
%and the resulting trees can be seen
%in Appendix~\ref{appendix}.

% In Lutovac's paper, it is said that they need to check if the active formula
% of the bottom rule is not a principal formula of the upper rule. It seems they
% are checking if two rules permute in an actual derivation and not
% generically...
% They also found a permutation between &/tensor.
The results were obtained relatively fast. Checking if two rules permute
(including the interaction with \texttt{dlv}) takes less than 0.05 seconds on
most of the cases. 
% Muuuch less... this was due to i/o (a million files beeing generated for
% debugging...)
%The longest running time encountered during the experiments
%was during the permutability check of $\oplus / \tensor$. Since the inference
%for $\oplus$ involves a non-deterministic choice of formula, the number of
%possible derivations is greater than other cases. This case took 0.16 seconds in average, which is
%still acceptable. 
The efficiency of \texttt{dlv} and the facility to process
its output played an important role in keeping a low running time.


